(* # =================================================================== 
   # FinType
   #
   # Introduction
   #
   # We build two types of the finite set of natural numbers with sig
   #
   # fin type is designed for the index of array :
   #
   #   fin n = { i : nat | i < n }. When n = 0, fin 0 = unit.
   #
   # fle type is designed for the verification of some rules about array :
   #
   #   fle n = { i : nat | i <= n }.
   #
   # The conversions between nat and the two types above are built by 
   #
   #   fin2nat, fle2nat, nat2fin, nat2fle.
   #
   # There are some properties between these functions.
   #
   #   fin2nat_nat2fin : forall n i , i < n -> fin2nat(nat2fin n i) = i.
   # 
   #   fin_eq : forall (n:nat) (i1 i2:fin n), fin2nat i1 = fin2nat i2 -> i1 = i2.
   #
   #   nat2fin_fin2nat : forall n (i:fin n) , nat2fin n (fin2nat i) = i
   #
   #   forall m x p, @fin2nat (S m) (exist (fun i : nat => i < (S m)) x p) = x.
   #
   #   fle_eq : forall (n:nat) (i1 i2:fle n), fle2nat i1 = fle2nat i2 -> i1 = i2.
   #
   #   fle2nat_exist: forall m x p, @fle2nat m (exist (fun i : nat => i <= m) x p) = x.
   # =================================================================== *)

Require Export Arith Lia.

Ltac inv H := intros; inversion H.

Section FiniteSetLt.

Local Open Scope nat_scope.

(* when n = 0, fin 0 = unit *)
Definition fin (n:nat) :Set :=
  match n with
  | 0 => unit
  | S n' =>  { i | i < (S n')}
  end. 

(* zero element in fin n *)
Definition fin_0 (n:nat): fin n :=
  match n with
  | O => tt
  | S n' => exist _ 0 (Nat.lt_0_succ n')
  end.


(* transform fin to nat *)
Definition fin2nat {n:nat} : fin n -> nat := 
   match n with
   | O => fun (i : fin O) => 0
   | S n' =>  fun (i : fin (S n')) => let (i0,_) := i in i0
  end.

(* transform nat to fin.  when i > n ,return  0: fin n *)
Definition nat2fin (n i:nat) : fin n :=
  match n with 
  | O => (tt:fin 0)
  | S n' => 
    match (le_lt_dec (S n') i) with
    | left k => (exist _ 0 (Nat.lt_0_succ n'):fin (S n'))
    | right k => exist _ i k  
    end
  end.

(* The relationship between fin2nat and nat2fin *)
Lemma fin2nat_nat2fin : forall n i ,
  i < n -> fin2nat(nat2fin n i) = i.
Proof.
  induction n. - lia. 
  - induction i. 
    + auto.
    + intros. destruct (le_lt_dec (S n) (S i)) eqn:E.
      lia. unfold nat2fin. rewrite E. auto.
Qed.

(* i+1:fin n *)
Definition finS {n:nat} (i:fin n): fin n :=
  nat2fin n (S (fin2nat i)).

Definition finPred {n:nat} (i:fin n) : fin n :=
  nat2fin n (pred (fin2nat i)).

Lemma finPredAux : forall {n:nat} (i:fin (S n)) , 0< fin2nat i ->
  pred (fin2nat i) < n.
Proof.
  induction i. simpl. intros. apply Nat.succ_lt_mono.
  rewrite <- S_pred_pos. auto. auto.
Qed.

Definition finPred' {n:nat} (i:fin (S n)) : fin n :=
  nat2fin n (pred (fin2nat i)).

(* i+m:fin n *)
Fixpoint finSn {n:nat} (i:fin n) (m:nat) : fin n :=
  match m with
  | O => i
  | S m' => finSn (finS i) m'
  end.

Example tmp_fin: 1<3. auto. Qed.

(* i:fin n -> i < S n *)
Lemma fin_finS_eq: forall (n:nat) (i:fin n), fin2nat i < (S n).
Proof.
  induction n. - auto. - simpl. intros. induction i. lia.
Qed.

(* fin n -> fin (S n) *)
Definition fin2finS {n:nat} (i : fin n) : fin (S n):=
  exist _ (fin2nat i) (fin_finS_eq n i).

Definition finS2fin  {n:nat} (i : fin (S n)) : fin n :=
  nat2fin n (fin2nat i).

(* the proof of m < n i is unique *)
Lemma lt_unique : forall m n (p1 p2: m < n),
  p1 = p2.
Proof. intros. unfold lt in p1,p2. apply le_unique. Qed.

(* the values of fin n equal then two (fin n) equal *)
Lemma fin_eq : forall (n:nat) (i1 i2:fin n),
  fin2nat i1 = fin2nat i2 -> i1 = i2.
Proof.
  induction n. - simpl. induction i1,i2. auto.
  - simpl. induction i1,i2. intros. subst. f_equal.
    apply lt_unique.
Qed.

Coercion fin2nat : fin >-> nat.

Lemma finltSn: forall n (i:fin (S n)),
  i < S n.
Proof. induction i. simpl. lia. Qed.

Lemma fin2nat_exist: forall m x p,
  @fin2nat (S m) (exist (fun i : nat => i < (S m)) x p) = x.
Proof. simpl. auto. Qed.

Lemma nat2fin_fin2nat : forall n (i:fin n) ,
  nat2fin n (fin2nat i) = i.
Proof.
  induction n. simpl. induction i. auto.
  induction i. rewrite fin2nat_exist. apply fin_eq.
  rewrite fin2nat_nat2fin,fin2nat_exist. auto. lia.
Qed.

Lemma fin_lt: forall n (x:fin n), n > 0 -> x < n.
Proof.
  induction n. lia. induction x. intros. simpl. lia.
Qed.

Lemma nat2fin_fin2finS : forall m x (i: fin x),
  S x <= m -> nat2fin m (fin2finS i) = nat2fin m i.
Proof.
  intros. simpl. auto. Qed.

Lemma fin2nat_fin2finS: forall(n:nat) (x:fin n) ,
  fin2nat(fin2finS x) = fin2nat x.
Proof.
  intros. unfold fin2finS. rewrite fin2nat_exist. auto.
Qed.

Lemma fin_le : forall m (i: fin m) , i <= m.
Proof.
  induction m. - simpl. lia. - induction i. simpl. lia.
Qed.

Lemma fin_lt': forall n m (i: fin n), n < m-> i < m.
Proof.
  induction n;auto;induction i;intros. rewrite fin2nat_exist.
  lia.
Qed.

Definition fin0: fin 0:= tt.

End FiniteSetLt.

Hint Rewrite fin2nat_nat2fin fin_eq nat2fin_fin2finS
  fin2nat_fin2finS fin2nat_exist.

Hint Resolve fin_finS_eq finltSn fin_lt fin_le fin_lt'
  fin2nat_exist fin2nat_fin2finS fin2nat_nat2fin fin_eq nat2fin_fin2finS .

Section FiniteSetLe.

(* fle i<=n *)
Definition fle (n:nat) := { i:nat | i<= n}.

Definition fle_self (n:nat) : fle n :=
  exist _ n (Nat.le_refl n).

Definition fle_0 (n:nat) : fle n :=
  exist _ 0 (Peano.le_0_n n).

Definition fle2nat {n:nat} (i:fle n) : nat :=
  let (a,b) := i in a.

Lemma fle2nat_fle_self: forall n,
  fle2nat (fle_self n) = n.
Proof.
  unfold fle_self. simpl. auto.
Qed. 

Lemma fle_eq : forall (n:nat) (i1 i2:fle n),
  fle2nat i1 = fle2nat i2 -> i1 = i2.
Proof.
  induction i1,i2. auto.
  simpl. intros. subst. f_equal. apply le_unique.
Qed. 

Definition nat2fle (n:nat) (i:nat) :fle n :=
  match (le_lt_dec i n) with
  | left p => exist _ i p
  | right p => fle_0 n
  end.

Coercion fle2nat : fle >-> nat.

Lemma le_lt_trans: forall m n p,
  m < n -> n <= p -> m < p.
Proof. lia. Qed.

Lemma flePredAux : forall (i:nat) ,0 < i -> pred i < i.
Proof. intros. apply lt_pred_n_n. auto. Qed. 

(* i - 1 : fin i*)
Definition flePred {m:nat} (i:fle m) : fin i :=
  match (fle2nat i) with
  | O => fin0
  | S i0 => exist _ i0 (flePredAux (S i0) (Nat.lt_0_succ i0) )
  end.

Lemma flePred'Aux : forall m (i:fle m), pred i <= m.
Proof.
  induction i. simpl. lia.
Qed.

Definition flePred' {m:nat} (i:fle m) :fle m :=
  exist _ (pred i) (flePred'Aux m i).

Lemma fle2nat_exist: forall m x p,
  @fle2nat m (exist (fun i : nat => i <= m) x p) = x.
Proof. simpl. auto. Qed.

End FiniteSetLe.

Hint Rewrite fle_eq fle2nat_exist fle2nat_fle_self.

Require Import Ascii String.

Section AuxFun.

Definition natToDigit (n : nat) : ascii :=
  match n with
    | 1 => "1"
    | 2 => "2"
    | 3 => "3"
    | 4 => "4"
    | 5 => "5"
    | 6 => "6"
    | 7 => "7"
    | 8 => "8"  
    | 9 => "9"
    | _ => "0"
  end.

Fixpoint writeNatAux (time n : nat) (acc : string) : string :=
  let acc' := String (natToDigit (n mod 10)) acc in
  match time with
    | 0 => acc'
    | S time' =>
      match n / 10 with
        | 0 => acc'
        | n' => writeNatAux time' n' acc'
      end
  end.

Definition writeNat (n : nat) : string :=
  writeNatAux n n "".

End AuxFun.
